The ACM–IEEE Symposium on Logic in Computer Science (LICS) is an annual

academic conference An academic conference or scientific conference (also congress, symposium, workshop, or meeting) is an event for researchers (not necessarily academics) to present and discuss their scholarly work. Together with academic or scientific journals an ...

on the theory and practice of

computer science Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to Applied science, practical discipli ...

in relation to

mathematical logic Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...

. Extended versions of selected papers of each year's conference appear in renowned international journals such as

Logical Methods in Computer Science ''Logical Methods in Computer Science'' (LMCS) is a peer-reviewed open access scientific journal covering theoretical computer science and applied logic. It opened to submissions on September 1, 2004. The editor-in-chief is Stefan Milius ( Fried ...

and

ACM Transactions on Computational Logic ''ACM Transactions on Computational Logic'' (''ACM TOCL'') is a scientific journal that aims to disseminate the latest findings of note in the field of logic in computer science. It is published by the Association for Computing Machinery, a premie ...

History

LICS was originally sponsored solely by the

IEEE The Institute of Electrical and Electronics Engineers (IEEE) is a 501(c)(3) professional association for electronic engineering and electrical engineering (and associated disciplines) with its corporate office in New York City and its operation ...

, but as of the 2014 founding of the ACM Special Interest Group on Logic and Computation LICS has become the flagship conference of SIGLOG, under the joint sponsorship of ACM and IEEE. From the first installment in 1988 until 2013, the cover page of the conference proceedings has featured an artwork entitled ''Irrational Tiling by Logical Quantifiers'', by Alvy Ray Smith. Since 1995, each year the '' Kleene award'' is given to the best student paper. In addition, since 2006, the ''LICS Test-of-Time Award'' is given annually to one among the twenty-year-old LICS papers that have best met the test of time.LICS awards website
/ref>

LICS Awards

Test-of-Time Award

Each year, since 2006, the LICS Test-of-Time Award recognizes those articles from LICS proceedings 20 years earlier, which have become influential.

2006

* Leo Bachmair,

Nachum Dershowitz Nachum Dershowitz is an Israeli computer scientist, known e.g. for the Dershowitz–Manna ordering and the multiset path ordering used to prove termination of term rewrite systems. He obtained his B.Sc. summa cum laude in 1974 in Computer Scie ...

, Jieh Hsiang, "Orderings for Equational Proofs" *

E. Allen Emerson Ernest Allen Emerson II (born June 2, 1954), better known as E. Allen Emerson, is an American computer scientist and winner of the 2007 Turing Award. He is Professor and Regents Chair Emeritus at the University of Texas at Austin, United States. ...

, Chin-Laung Lei, "Efficient Model Checking in Fragments of the Propositional Mu-Calculus (Extended Abstract)" *

Moshe Y. Vardi , honorific_suffix = , image = Moshe Vardi IMG 0010.jpg , birth_date = , birth_place = Israel , workplaces = Rice UniversityIBM ResearchStanford University , alma_mater = , thesis_title = The I ...

Pierre Wolper Pierre Wolper is a Belgian computer scientist at the University of Liège. His research interests include verification methods for reactive and concurrent programs, as well as temporal databases. He is the co-recipient of the 2000 Gödel Prize, al ...

, "An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report)"

2007

Samson Abramsky Samson Abramsky (born 12 March 1953) is Professor of Computer Science at University College London. He was previously the Christopher Strachey Professor of Computing at the University of Oxford, from 2000 to 2021. He has made contributions to t ...

, "Domain theory in Logical Form" *

Robert Harper Robert or Bob Harper may refer to: * Robert Almer Harper (1862–1946), American botanist * Robert Goodloe Harper (1765–1825), US senator from Maryland * Robert Harper (fl. 1734–1761), founder of Harpers Ferry, West Virginia * Robert Harper (a ...

, Furio Honsell, Gordon D. Plotkin, "A Framework for Defining Logics"

2008

Martin Abadi Martin may refer to: Places * Martin City (disambiguation) * Martin County (disambiguation) * Martin Township (disambiguation) Antarctica * Martin Peninsula, Marie Byrd Land * Port Martin, Adelie Land * Point Martin, South Orkney Islands Austral ...

Leslie Lamport Leslie B. Lamport (born February 7, 1941 in Brooklyn) is an American computer scientist and mathematician. Lamport is best known for his seminal work in distributed systems, and as the initial developer of the document preparation system LaTeX and ...

, "The existence of refinement mappings"

2009

Eugenio Moggi Eugenio Moggi is a professor of computer science at the University of Genoa, Italy. He first described the general use of monads to structure programs. Biography Academic qualifications: * PhD in Computer Science, University of Edinburgh 19 ...

, "Computational lambda-calculus and monads"

2010

Rajeev Alur Rajeev Alur is an American professor of computer science at the University of Pennsylvania who has made contributions to formal methods, programming languages, and automata theory, including notably the introduction of timed automata (Alur and Dil ...

Costas Courcoubetis Kostas or Costas ( el, Κώστας) is a Greek given name and surname. As a given name it is the hypocorism for Konstantinos (Constantine). Given name * Costas Andreou, Greek musician * Kostas Antetokounmpo (born 1997), a Greek basketball player ...

, David L. Dill, "Model-checking for real-time systems" * Jerry R. Burch,

Edmund Clarke Edmund Melson Clarke, Jr. (July 27, 1945 – December 22, 2020) was an American computer scientist and academic noted for developing model checking, a method for formally verifying hardware and software designs. He was the FORE Systems Professor ...

, Kenneth L. McMillan, David L. Dill,

James Hwang James is a common English language surname and given name: *James (name), the typically masculine first name James * James (surname), various people with the last name James James or James City may also refer to: People * King James (disambiguat ...

, "Symbolic model checking: 10^20 states and beyond" *

Max Dauchet Max or MAX may refer to: Animals * Max (dog) (1983–2013), at one time purported to be the world's oldest living dog * Max (English Springer Spaniel), the first pet dog to win the PDSA Order of Merit (animal equivalent of OBE) * Max (gorilla) ...

Sophie Tison Sophie is a version of the female given name Sophia (given name), Sophia, meaning "wise". People with the name Born in the Middle Ages * Sophie, Countess of Bar (c. 1004 or 1018–1093), sovereign Countess of Bar and lady of Mousson * Sophie of T ...

, "The theory of ground rewrite systems is decidable" *

Peter Freyd Peter John Freyd (; born February 5, 1936) is an American mathematician, a professor at the University of Pennsylvania, known for work in category theory and for founding the False Memory Syndrome Foundation. Mathematics Freyd obtained his P ...

, "Recursive types reduced to inductive types"

2011

* Patrice Godefroid,

, "A partial approach to model checking" * Joshua Hodas, Dale A. Miller, "Logic programming in a fragment of intuitionistic linear logic" *

Dexter Kozen Dexter Campbell Kozen (born December 20, 1951) is an American theoretical computer scientist. He is Joseph Newton Pew, Jr. Professor in Engineering at Cornell University. He received his B.A. from Dartmouth College in 1974 and his PhD in compute ...

, "A completeness theorem for Kleene algebras and the algebra of regular events"

2012

Thomas Henzinger Thomas Henzinger (born 1962) is an Austrian computer scientist, researcher, and president of the Institute of Science and Technology, Austria. Life and career Henzinger was born in Austria. He received his bachelor's degree in computer science ...

, Xavier Nicollin,

Joseph Sifakis Joseph Sifakis (Greek: Ιωσήφ Σηφάκης) is a Greek-French computer scientist. He received the 2007 Turing Award, along with Edmund M. Clarke and E. Allen Emerson, for his work on model checking. Biography Joseph Sifakis was born in H ...

, Sergio Yovine, "Symbolic model checking for real-time systems" *

Jean-Pierre Talpin Jean-Pierre or Jean Pierre may refer to: People * Karine Jean-Pierre b.1977, White House Deputy Press Secretary for President Joe Biden 2021- * Jean-Pierre, Count of Montalivet (1766–1823), French statesman and Peer of France * Eugenia Pierre ...

, Pierre Jouvelot, "The type and effect discipline"

2013

* Leo Bachmair,

Harald Ganzinger Harald Ganzinger (31 October 1950, Werneck – 3 June 2004, Saarbrücken) was a German computer scientist who together with Leo Bachmair developed the superposition calculus, which is (as of 2007) used in most of the state-of-the-art automated ...

, Uwe Waldmann, "Set constraints are the monadic class" *

André Joyal André Joyal (; born 1943) is a professor of mathematics at the Université du Québec à Montréal who works on category theory. He was a member of the School of Mathematics at the Institute for Advanced Study in 2013, where he was invited to jo ...

, Mogens Nielson, Glynn Winskel, "Bisimulation and open maps" * Benjamin C. Pierce,

Davide Sangiorgi Davide Sangiorgi is an Italian professor of computer science at the University of Bologna. He has previously held research positions at the University of Edinburgh and at Inria. He has received his PhD from the University of Edinburgh under the s ...

, "Typing and subtyping for mobile processes"

2014

* Martin Hofmann, Thomas Streicher, "The groupoid model refutes uniqueness of identity proofs" * Dale A. Miller, "A multiple-conclusion meta-logic"

2015

* Igor Walukiewicz, "Completeness of Kozen's Axiomatisation of the Propositional Mu-Calculus"

2016

* Parosh A. Abdulla, Karlis Cerans, Bengt Jonsson, Yih-Kuen Tsay, "General decidability theorems for infinite-state systems" * Iliano Cervesato,

Frank Pfenning Frank Pfenning is a German-American professor of computer science, adjunct professor in the department of philosophy, and head of the Computer Science Department at Carnegie Mellon University. Education and career Pfenning grew up in Rüssel ...

, "A Linear Logical Framework"

2017

* Richard Blute, Josée Desharnais,

Abbas Edalat Abbas Edalat ( fa, عباس عدالت) is a British-Iranian academic who is a professor of computer science and mathematics at the Department of Computing, Imperial College London and a political activist. In a 2018 letter to The Guardian, 1 ...

Prakash Panangaden Prakash Panangaden is an American/Canadian computer scientist noted for his research in programming language theory, concurrency theory, Markov processes and duality theory. Earlier he worked on quantum field theory in curved space-time and radia ...

, "Bisimulation for Labelled Markov Processes" * Daniele Turi, Gordon D. Plotkin, "Towards a Mathematical Operational Semantics"

2018

* Martín Abadi, Cédric Fournet,

Georges Gonthier Georges Gonthier is a Canadian computer scientist and one of the leading practitioners in formal mathematics. He led the formalization of the four color theorem and Feit–Thompson proof of the odd-order theorem. (Both were written using the ...

, "Secure Implementation of Channel Abstractions" *

, Kohei Honda, Guy McCusker, "A Fully Abstract Game Semantics for General References"

2019

* Marcelo P. Fiore, Gordon D. Plotkin, Daniele Turi, "Abstract Syntax and Variable Binding" * Murdoch Gabbay, Andrew M. Pitts, "A New Approach to Abstract Syntax Involving Binders"

2020

* Luca de Alfaro, Thomas A. Henzinger, "Concurrent Omega-Regular Games" * Hiroshi Nakano, "A Modality for Recursion"

2021

* Aaron Stump;, Clark W. Barrett, David L. Dill, Jeremy R. Levitt, "A Decision Procedure for an Extensional Theory of Arrays" *

Hongwei Xi Hongwei District () is a district of Liaoyang City, Liaoning province, People's Republic of China. Administrative Divisions There are four Subdistrict (China), subdistricts and one Town (China), town within the district. Subdistricts: *Changzheng ...

, "Dependent Types for Program Termination Verification"

Kleene award

At each conference the Kleene award, in honour of S.C. Kleene, is given for the best student paper.

Notes

External links

LICS home page
{{Authority control Theoretical computer science conferences Logic conferences Logic in computer science IEEE conferences